r:, L:Top List. ||nth_tl(r;L)|| = if r<||L|| ||L||-r else 0 fi   

latex

Definitions	tl(l), i<j, ij, , t  T, x:A. B(x), P  Q, ij, Top, False, A, AB, ||as||, Prop, True, b, b, , T, P  Q, P & Q, P  Q, Unit, if b t else f fi, nth_tl(n;as), {T}, SQType(T)
Lemmas	length cons, tl wf, ifthenelse wf, length tl, nth tl wf, bnot of le int, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, lt int wf, length wf1, top wf, bool wf, le int wf, le wf, assert wf, bnot wf, non neg length, ge wf, nat properties, nat wf